↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
g_in(W) → U1(W, eq_in(X, .(.(a, []), .(.(R, []), []))))
eq_in(X, X) → eq_out(X, X)
U1(W, eq_out(X, .(.(a, []), .(.(R, []), [])))) → U2(W, X, eq_in(Y, .(.(S, .(c, [])), .([], []))))
U2(W, X, eq_out(Y, .(.(S, .(c, [])), .([], [])))) → U3(W, app_1_in(X, Y, Z))
app_1_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_1_in(Xs, Ys, Zs))
app_1_in([], X, X) → app_1_out([], X, X)
U6(X, Xs, Ys, Zs, app_1_out(Xs, Ys, Zs)) → app_1_out(.(X, Xs), Ys, .(X, Zs))
U3(W, app_1_out(X, Y, Z)) → U4(W, eq_in(Z, .(U, V)))
U4(W, eq_out(Z, .(U, V))) → U5(W, app_2_in(U, U, W))
app_2_in(.(X, Xs), Ys, .(X, Zs)) → U7(X, Xs, Ys, Zs, app_2_in(Xs, Ys, Zs))
app_2_in([], X, X) → app_2_out([], X, X)
U7(X, Xs, Ys, Zs, app_2_out(Xs, Ys, Zs)) → app_2_out(.(X, Xs), Ys, .(X, Zs))
U5(W, app_2_out(U, U, W)) → g_out(W)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PrologToPiTRSProof
g_in(W) → U1(W, eq_in(X, .(.(a, []), .(.(R, []), []))))
eq_in(X, X) → eq_out(X, X)
U1(W, eq_out(X, .(.(a, []), .(.(R, []), [])))) → U2(W, X, eq_in(Y, .(.(S, .(c, [])), .([], []))))
U2(W, X, eq_out(Y, .(.(S, .(c, [])), .([], [])))) → U3(W, app_1_in(X, Y, Z))
app_1_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_1_in(Xs, Ys, Zs))
app_1_in([], X, X) → app_1_out([], X, X)
U6(X, Xs, Ys, Zs, app_1_out(Xs, Ys, Zs)) → app_1_out(.(X, Xs), Ys, .(X, Zs))
U3(W, app_1_out(X, Y, Z)) → U4(W, eq_in(Z, .(U, V)))
U4(W, eq_out(Z, .(U, V))) → U5(W, app_2_in(U, U, W))
app_2_in(.(X, Xs), Ys, .(X, Zs)) → U7(X, Xs, Ys, Zs, app_2_in(Xs, Ys, Zs))
app_2_in([], X, X) → app_2_out([], X, X)
U7(X, Xs, Ys, Zs, app_2_out(Xs, Ys, Zs)) → app_2_out(.(X, Xs), Ys, .(X, Zs))
U5(W, app_2_out(U, U, W)) → g_out(W)
G_IN(W) → U11(W, eq_in(X, .(.(a, []), .(.(R, []), []))))
G_IN(W) → EQ_IN(X, .(.(a, []), .(.(R, []), [])))
U11(W, eq_out(X, .(.(a, []), .(.(R, []), [])))) → U21(W, X, eq_in(Y, .(.(S, .(c, [])), .([], []))))
U11(W, eq_out(X, .(.(a, []), .(.(R, []), [])))) → EQ_IN(Y, .(.(S, .(c, [])), .([], [])))
U21(W, X, eq_out(Y, .(.(S, .(c, [])), .([], [])))) → U31(W, app_1_in(X, Y, Z))
U21(W, X, eq_out(Y, .(.(S, .(c, [])), .([], [])))) → APP_1_IN(X, Y, Z)
APP_1_IN(.(X, Xs), Ys, .(X, Zs)) → U61(X, Xs, Ys, Zs, app_1_in(Xs, Ys, Zs))
APP_1_IN(.(X, Xs), Ys, .(X, Zs)) → APP_1_IN(Xs, Ys, Zs)
U31(W, app_1_out(X, Y, Z)) → U41(W, eq_in(Z, .(U, V)))
U31(W, app_1_out(X, Y, Z)) → EQ_IN(Z, .(U, V))
U41(W, eq_out(Z, .(U, V))) → U51(W, app_2_in(U, U, W))
U41(W, eq_out(Z, .(U, V))) → APP_2_IN(U, U, W)
APP_2_IN(.(X, Xs), Ys, .(X, Zs)) → U71(X, Xs, Ys, Zs, app_2_in(Xs, Ys, Zs))
APP_2_IN(.(X, Xs), Ys, .(X, Zs)) → APP_2_IN(Xs, Ys, Zs)
g_in(W) → U1(W, eq_in(X, .(.(a, []), .(.(R, []), []))))
eq_in(X, X) → eq_out(X, X)
U1(W, eq_out(X, .(.(a, []), .(.(R, []), [])))) → U2(W, X, eq_in(Y, .(.(S, .(c, [])), .([], []))))
U2(W, X, eq_out(Y, .(.(S, .(c, [])), .([], [])))) → U3(W, app_1_in(X, Y, Z))
app_1_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_1_in(Xs, Ys, Zs))
app_1_in([], X, X) → app_1_out([], X, X)
U6(X, Xs, Ys, Zs, app_1_out(Xs, Ys, Zs)) → app_1_out(.(X, Xs), Ys, .(X, Zs))
U3(W, app_1_out(X, Y, Z)) → U4(W, eq_in(Z, .(U, V)))
U4(W, eq_out(Z, .(U, V))) → U5(W, app_2_in(U, U, W))
app_2_in(.(X, Xs), Ys, .(X, Zs)) → U7(X, Xs, Ys, Zs, app_2_in(Xs, Ys, Zs))
app_2_in([], X, X) → app_2_out([], X, X)
U7(X, Xs, Ys, Zs, app_2_out(Xs, Ys, Zs)) → app_2_out(.(X, Xs), Ys, .(X, Zs))
U5(W, app_2_out(U, U, W)) → g_out(W)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PrologToPiTRSProof
G_IN(W) → U11(W, eq_in(X, .(.(a, []), .(.(R, []), []))))
G_IN(W) → EQ_IN(X, .(.(a, []), .(.(R, []), [])))
U11(W, eq_out(X, .(.(a, []), .(.(R, []), [])))) → U21(W, X, eq_in(Y, .(.(S, .(c, [])), .([], []))))
U11(W, eq_out(X, .(.(a, []), .(.(R, []), [])))) → EQ_IN(Y, .(.(S, .(c, [])), .([], [])))
U21(W, X, eq_out(Y, .(.(S, .(c, [])), .([], [])))) → U31(W, app_1_in(X, Y, Z))
U21(W, X, eq_out(Y, .(.(S, .(c, [])), .([], [])))) → APP_1_IN(X, Y, Z)
APP_1_IN(.(X, Xs), Ys, .(X, Zs)) → U61(X, Xs, Ys, Zs, app_1_in(Xs, Ys, Zs))
APP_1_IN(.(X, Xs), Ys, .(X, Zs)) → APP_1_IN(Xs, Ys, Zs)
U31(W, app_1_out(X, Y, Z)) → U41(W, eq_in(Z, .(U, V)))
U31(W, app_1_out(X, Y, Z)) → EQ_IN(Z, .(U, V))
U41(W, eq_out(Z, .(U, V))) → U51(W, app_2_in(U, U, W))
U41(W, eq_out(Z, .(U, V))) → APP_2_IN(U, U, W)
APP_2_IN(.(X, Xs), Ys, .(X, Zs)) → U71(X, Xs, Ys, Zs, app_2_in(Xs, Ys, Zs))
APP_2_IN(.(X, Xs), Ys, .(X, Zs)) → APP_2_IN(Xs, Ys, Zs)
g_in(W) → U1(W, eq_in(X, .(.(a, []), .(.(R, []), []))))
eq_in(X, X) → eq_out(X, X)
U1(W, eq_out(X, .(.(a, []), .(.(R, []), [])))) → U2(W, X, eq_in(Y, .(.(S, .(c, [])), .([], []))))
U2(W, X, eq_out(Y, .(.(S, .(c, [])), .([], [])))) → U3(W, app_1_in(X, Y, Z))
app_1_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_1_in(Xs, Ys, Zs))
app_1_in([], X, X) → app_1_out([], X, X)
U6(X, Xs, Ys, Zs, app_1_out(Xs, Ys, Zs)) → app_1_out(.(X, Xs), Ys, .(X, Zs))
U3(W, app_1_out(X, Y, Z)) → U4(W, eq_in(Z, .(U, V)))
U4(W, eq_out(Z, .(U, V))) → U5(W, app_2_in(U, U, W))
app_2_in(.(X, Xs), Ys, .(X, Zs)) → U7(X, Xs, Ys, Zs, app_2_in(Xs, Ys, Zs))
app_2_in([], X, X) → app_2_out([], X, X)
U7(X, Xs, Ys, Zs, app_2_out(Xs, Ys, Zs)) → app_2_out(.(X, Xs), Ys, .(X, Zs))
U5(W, app_2_out(U, U, W)) → g_out(W)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PrologToPiTRSProof
APP_2_IN(.(X, Xs), Ys, .(X, Zs)) → APP_2_IN(Xs, Ys, Zs)
g_in(W) → U1(W, eq_in(X, .(.(a, []), .(.(R, []), []))))
eq_in(X, X) → eq_out(X, X)
U1(W, eq_out(X, .(.(a, []), .(.(R, []), [])))) → U2(W, X, eq_in(Y, .(.(S, .(c, [])), .([], []))))
U2(W, X, eq_out(Y, .(.(S, .(c, [])), .([], [])))) → U3(W, app_1_in(X, Y, Z))
app_1_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_1_in(Xs, Ys, Zs))
app_1_in([], X, X) → app_1_out([], X, X)
U6(X, Xs, Ys, Zs, app_1_out(Xs, Ys, Zs)) → app_1_out(.(X, Xs), Ys, .(X, Zs))
U3(W, app_1_out(X, Y, Z)) → U4(W, eq_in(Z, .(U, V)))
U4(W, eq_out(Z, .(U, V))) → U5(W, app_2_in(U, U, W))
app_2_in(.(X, Xs), Ys, .(X, Zs)) → U7(X, Xs, Ys, Zs, app_2_in(Xs, Ys, Zs))
app_2_in([], X, X) → app_2_out([], X, X)
U7(X, Xs, Ys, Zs, app_2_out(Xs, Ys, Zs)) → app_2_out(.(X, Xs), Ys, .(X, Zs))
U5(W, app_2_out(U, U, W)) → g_out(W)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PrologToPiTRSProof
APP_2_IN(.(X, Xs), Ys, .(X, Zs)) → APP_2_IN(Xs, Ys, Zs)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ NonTerminationProof
↳ PiDP
↳ PrologToPiTRSProof
APP_2_IN → APP_2_IN
APP_2_IN → APP_2_IN
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PrologToPiTRSProof
APP_1_IN(.(X, Xs), Ys, .(X, Zs)) → APP_1_IN(Xs, Ys, Zs)
g_in(W) → U1(W, eq_in(X, .(.(a, []), .(.(R, []), []))))
eq_in(X, X) → eq_out(X, X)
U1(W, eq_out(X, .(.(a, []), .(.(R, []), [])))) → U2(W, X, eq_in(Y, .(.(S, .(c, [])), .([], []))))
U2(W, X, eq_out(Y, .(.(S, .(c, [])), .([], [])))) → U3(W, app_1_in(X, Y, Z))
app_1_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_1_in(Xs, Ys, Zs))
app_1_in([], X, X) → app_1_out([], X, X)
U6(X, Xs, Ys, Zs, app_1_out(Xs, Ys, Zs)) → app_1_out(.(X, Xs), Ys, .(X, Zs))
U3(W, app_1_out(X, Y, Z)) → U4(W, eq_in(Z, .(U, V)))
U4(W, eq_out(Z, .(U, V))) → U5(W, app_2_in(U, U, W))
app_2_in(.(X, Xs), Ys, .(X, Zs)) → U7(X, Xs, Ys, Zs, app_2_in(Xs, Ys, Zs))
app_2_in([], X, X) → app_2_out([], X, X)
U7(X, Xs, Ys, Zs, app_2_out(Xs, Ys, Zs)) → app_2_out(.(X, Xs), Ys, .(X, Zs))
U5(W, app_2_out(U, U, W)) → g_out(W)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PrologToPiTRSProof
APP_1_IN(.(X, Xs), Ys, .(X, Zs)) → APP_1_IN(Xs, Ys, Zs)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ NonTerminationProof
↳ PrologToPiTRSProof
APP_1_IN → APP_1_IN
APP_1_IN → APP_1_IN
g_in(W) → U1(W, eq_in(X, .(.(a, []), .(.(R, []), []))))
eq_in(X, X) → eq_out(X, X)
U1(W, eq_out(X, .(.(a, []), .(.(R, []), [])))) → U2(W, X, eq_in(Y, .(.(S, .(c, [])), .([], []))))
U2(W, X, eq_out(Y, .(.(S, .(c, [])), .([], [])))) → U3(W, app_1_in(X, Y, Z))
app_1_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_1_in(Xs, Ys, Zs))
app_1_in([], X, X) → app_1_out([], X, X)
U6(X, Xs, Ys, Zs, app_1_out(Xs, Ys, Zs)) → app_1_out(.(X, Xs), Ys, .(X, Zs))
U3(W, app_1_out(X, Y, Z)) → U4(W, eq_in(Z, .(U, V)))
U4(W, eq_out(Z, .(U, V))) → U5(W, app_2_in(U, U, W))
app_2_in(.(X, Xs), Ys, .(X, Zs)) → U7(X, Xs, Ys, Zs, app_2_in(Xs, Ys, Zs))
app_2_in([], X, X) → app_2_out([], X, X)
U7(X, Xs, Ys, Zs, app_2_out(Xs, Ys, Zs)) → app_2_out(.(X, Xs), Ys, .(X, Zs))
U5(W, app_2_out(U, U, W)) → g_out(W)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
g_in(W) → U1(W, eq_in(X, .(.(a, []), .(.(R, []), []))))
eq_in(X, X) → eq_out(X, X)
U1(W, eq_out(X, .(.(a, []), .(.(R, []), [])))) → U2(W, X, eq_in(Y, .(.(S, .(c, [])), .([], []))))
U2(W, X, eq_out(Y, .(.(S, .(c, [])), .([], [])))) → U3(W, app_1_in(X, Y, Z))
app_1_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_1_in(Xs, Ys, Zs))
app_1_in([], X, X) → app_1_out([], X, X)
U6(X, Xs, Ys, Zs, app_1_out(Xs, Ys, Zs)) → app_1_out(.(X, Xs), Ys, .(X, Zs))
U3(W, app_1_out(X, Y, Z)) → U4(W, eq_in(Z, .(U, V)))
U4(W, eq_out(Z, .(U, V))) → U5(W, app_2_in(U, U, W))
app_2_in(.(X, Xs), Ys, .(X, Zs)) → U7(X, Xs, Ys, Zs, app_2_in(Xs, Ys, Zs))
app_2_in([], X, X) → app_2_out([], X, X)
U7(X, Xs, Ys, Zs, app_2_out(Xs, Ys, Zs)) → app_2_out(.(X, Xs), Ys, .(X, Zs))
U5(W, app_2_out(U, U, W)) → g_out(W)
G_IN(W) → U11(W, eq_in(X, .(.(a, []), .(.(R, []), []))))
G_IN(W) → EQ_IN(X, .(.(a, []), .(.(R, []), [])))
U11(W, eq_out(X, .(.(a, []), .(.(R, []), [])))) → U21(W, X, eq_in(Y, .(.(S, .(c, [])), .([], []))))
U11(W, eq_out(X, .(.(a, []), .(.(R, []), [])))) → EQ_IN(Y, .(.(S, .(c, [])), .([], [])))
U21(W, X, eq_out(Y, .(.(S, .(c, [])), .([], [])))) → U31(W, app_1_in(X, Y, Z))
U21(W, X, eq_out(Y, .(.(S, .(c, [])), .([], [])))) → APP_1_IN(X, Y, Z)
APP_1_IN(.(X, Xs), Ys, .(X, Zs)) → U61(X, Xs, Ys, Zs, app_1_in(Xs, Ys, Zs))
APP_1_IN(.(X, Xs), Ys, .(X, Zs)) → APP_1_IN(Xs, Ys, Zs)
U31(W, app_1_out(X, Y, Z)) → U41(W, eq_in(Z, .(U, V)))
U31(W, app_1_out(X, Y, Z)) → EQ_IN(Z, .(U, V))
U41(W, eq_out(Z, .(U, V))) → U51(W, app_2_in(U, U, W))
U41(W, eq_out(Z, .(U, V))) → APP_2_IN(U, U, W)
APP_2_IN(.(X, Xs), Ys, .(X, Zs)) → U71(X, Xs, Ys, Zs, app_2_in(Xs, Ys, Zs))
APP_2_IN(.(X, Xs), Ys, .(X, Zs)) → APP_2_IN(Xs, Ys, Zs)
g_in(W) → U1(W, eq_in(X, .(.(a, []), .(.(R, []), []))))
eq_in(X, X) → eq_out(X, X)
U1(W, eq_out(X, .(.(a, []), .(.(R, []), [])))) → U2(W, X, eq_in(Y, .(.(S, .(c, [])), .([], []))))
U2(W, X, eq_out(Y, .(.(S, .(c, [])), .([], [])))) → U3(W, app_1_in(X, Y, Z))
app_1_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_1_in(Xs, Ys, Zs))
app_1_in([], X, X) → app_1_out([], X, X)
U6(X, Xs, Ys, Zs, app_1_out(Xs, Ys, Zs)) → app_1_out(.(X, Xs), Ys, .(X, Zs))
U3(W, app_1_out(X, Y, Z)) → U4(W, eq_in(Z, .(U, V)))
U4(W, eq_out(Z, .(U, V))) → U5(W, app_2_in(U, U, W))
app_2_in(.(X, Xs), Ys, .(X, Zs)) → U7(X, Xs, Ys, Zs, app_2_in(Xs, Ys, Zs))
app_2_in([], X, X) → app_2_out([], X, X)
U7(X, Xs, Ys, Zs, app_2_out(Xs, Ys, Zs)) → app_2_out(.(X, Xs), Ys, .(X, Zs))
U5(W, app_2_out(U, U, W)) → g_out(W)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
G_IN(W) → U11(W, eq_in(X, .(.(a, []), .(.(R, []), []))))
G_IN(W) → EQ_IN(X, .(.(a, []), .(.(R, []), [])))
U11(W, eq_out(X, .(.(a, []), .(.(R, []), [])))) → U21(W, X, eq_in(Y, .(.(S, .(c, [])), .([], []))))
U11(W, eq_out(X, .(.(a, []), .(.(R, []), [])))) → EQ_IN(Y, .(.(S, .(c, [])), .([], [])))
U21(W, X, eq_out(Y, .(.(S, .(c, [])), .([], [])))) → U31(W, app_1_in(X, Y, Z))
U21(W, X, eq_out(Y, .(.(S, .(c, [])), .([], [])))) → APP_1_IN(X, Y, Z)
APP_1_IN(.(X, Xs), Ys, .(X, Zs)) → U61(X, Xs, Ys, Zs, app_1_in(Xs, Ys, Zs))
APP_1_IN(.(X, Xs), Ys, .(X, Zs)) → APP_1_IN(Xs, Ys, Zs)
U31(W, app_1_out(X, Y, Z)) → U41(W, eq_in(Z, .(U, V)))
U31(W, app_1_out(X, Y, Z)) → EQ_IN(Z, .(U, V))
U41(W, eq_out(Z, .(U, V))) → U51(W, app_2_in(U, U, W))
U41(W, eq_out(Z, .(U, V))) → APP_2_IN(U, U, W)
APP_2_IN(.(X, Xs), Ys, .(X, Zs)) → U71(X, Xs, Ys, Zs, app_2_in(Xs, Ys, Zs))
APP_2_IN(.(X, Xs), Ys, .(X, Zs)) → APP_2_IN(Xs, Ys, Zs)
g_in(W) → U1(W, eq_in(X, .(.(a, []), .(.(R, []), []))))
eq_in(X, X) → eq_out(X, X)
U1(W, eq_out(X, .(.(a, []), .(.(R, []), [])))) → U2(W, X, eq_in(Y, .(.(S, .(c, [])), .([], []))))
U2(W, X, eq_out(Y, .(.(S, .(c, [])), .([], [])))) → U3(W, app_1_in(X, Y, Z))
app_1_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_1_in(Xs, Ys, Zs))
app_1_in([], X, X) → app_1_out([], X, X)
U6(X, Xs, Ys, Zs, app_1_out(Xs, Ys, Zs)) → app_1_out(.(X, Xs), Ys, .(X, Zs))
U3(W, app_1_out(X, Y, Z)) → U4(W, eq_in(Z, .(U, V)))
U4(W, eq_out(Z, .(U, V))) → U5(W, app_2_in(U, U, W))
app_2_in(.(X, Xs), Ys, .(X, Zs)) → U7(X, Xs, Ys, Zs, app_2_in(Xs, Ys, Zs))
app_2_in([], X, X) → app_2_out([], X, X)
U7(X, Xs, Ys, Zs, app_2_out(Xs, Ys, Zs)) → app_2_out(.(X, Xs), Ys, .(X, Zs))
U5(W, app_2_out(U, U, W)) → g_out(W)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
APP_2_IN(.(X, Xs), Ys, .(X, Zs)) → APP_2_IN(Xs, Ys, Zs)
g_in(W) → U1(W, eq_in(X, .(.(a, []), .(.(R, []), []))))
eq_in(X, X) → eq_out(X, X)
U1(W, eq_out(X, .(.(a, []), .(.(R, []), [])))) → U2(W, X, eq_in(Y, .(.(S, .(c, [])), .([], []))))
U2(W, X, eq_out(Y, .(.(S, .(c, [])), .([], [])))) → U3(W, app_1_in(X, Y, Z))
app_1_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_1_in(Xs, Ys, Zs))
app_1_in([], X, X) → app_1_out([], X, X)
U6(X, Xs, Ys, Zs, app_1_out(Xs, Ys, Zs)) → app_1_out(.(X, Xs), Ys, .(X, Zs))
U3(W, app_1_out(X, Y, Z)) → U4(W, eq_in(Z, .(U, V)))
U4(W, eq_out(Z, .(U, V))) → U5(W, app_2_in(U, U, W))
app_2_in(.(X, Xs), Ys, .(X, Zs)) → U7(X, Xs, Ys, Zs, app_2_in(Xs, Ys, Zs))
app_2_in([], X, X) → app_2_out([], X, X)
U7(X, Xs, Ys, Zs, app_2_out(Xs, Ys, Zs)) → app_2_out(.(X, Xs), Ys, .(X, Zs))
U5(W, app_2_out(U, U, W)) → g_out(W)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
APP_2_IN(.(X, Xs), Ys, .(X, Zs)) → APP_2_IN(Xs, Ys, Zs)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ NonTerminationProof
↳ PiDP
APP_2_IN → APP_2_IN
APP_2_IN → APP_2_IN
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
APP_1_IN(.(X, Xs), Ys, .(X, Zs)) → APP_1_IN(Xs, Ys, Zs)
g_in(W) → U1(W, eq_in(X, .(.(a, []), .(.(R, []), []))))
eq_in(X, X) → eq_out(X, X)
U1(W, eq_out(X, .(.(a, []), .(.(R, []), [])))) → U2(W, X, eq_in(Y, .(.(S, .(c, [])), .([], []))))
U2(W, X, eq_out(Y, .(.(S, .(c, [])), .([], [])))) → U3(W, app_1_in(X, Y, Z))
app_1_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_1_in(Xs, Ys, Zs))
app_1_in([], X, X) → app_1_out([], X, X)
U6(X, Xs, Ys, Zs, app_1_out(Xs, Ys, Zs)) → app_1_out(.(X, Xs), Ys, .(X, Zs))
U3(W, app_1_out(X, Y, Z)) → U4(W, eq_in(Z, .(U, V)))
U4(W, eq_out(Z, .(U, V))) → U5(W, app_2_in(U, U, W))
app_2_in(.(X, Xs), Ys, .(X, Zs)) → U7(X, Xs, Ys, Zs, app_2_in(Xs, Ys, Zs))
app_2_in([], X, X) → app_2_out([], X, X)
U7(X, Xs, Ys, Zs, app_2_out(Xs, Ys, Zs)) → app_2_out(.(X, Xs), Ys, .(X, Zs))
U5(W, app_2_out(U, U, W)) → g_out(W)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
APP_1_IN(.(X, Xs), Ys, .(X, Zs)) → APP_1_IN(Xs, Ys, Zs)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ NonTerminationProof
APP_1_IN → APP_1_IN
APP_1_IN → APP_1_IN